package controller.preprocessor;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.Scanner;
import java.util.concurrent.Semaphore;

import model.cnf.FileCNF;
import model.cnf.Stat;
import model.preprocessor.EPreProcessor;
import model.preprocessor.PreProcessorParameter;
import model.preprocessor.PreProcessorResult;
import model.preprocessor.PreProcessorResultStatus;
import model.preprocessor.Satellite_1_0Parameter;

/**
 * This class is a implementation of PreProcessor for Satellite 1.0.
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class SatEllite1_0 extends PreProcessor {

	public static final String		EXEC					= "SatELite_v1.0";
	public static final String		DESCRIPTION				= "Result of the SatELite_v1.0 execution";
	public static final String		LITERALS				= "#literals: ";

	/** The default value that is return */
	public static final int			DEFAULT_RETURN_VALUE	= 0;
	/** The default value that is associate to a UNSATISFIABLE result */
	public static final int			RETURN_UNSATISFIABLE	= 20;

	private Satellite_1_0Parameter	param;

	/**
	 * Create a satellite 1.0 preprocessor.
	 * 
	 * @param directory
	 *            directory where the executable file is.
	 * @throws IOException
	 *             if there is a problem with the file.
	 */
	public SatEllite1_0(File directory) throws IOException {
		if (!directory.isDirectory() || !new File(directory, EXEC).isFile())
			throw new IllegalArgumentException();

		param = new Satellite_1_0Parameter();
		type = EPreProcessor.SATELLITE_1_0;

		try
		{
			path = directory.getCanonicalPath() + File.separator + EXEC;
		} catch (IOException e)
		{
			e.printStackTrace();
			throw new IOException();
		}
	}

	@Override
	public boolean checkParameter() {
		return param.basicCheck();
	}

	@Override
	public PreProcessorParameter getPreProcessorParameter() {
		return param;
	}

	/**
	 * 
	 * @return the satellite parameter
	 */
	public Satellite_1_0Parameter getSatelliteParameter() {
		return param;
	}

	@Override
	public String[] getCommandLine(String cnfFile) {
		String[] tab = new String[3];

		// bash
		tab[0] = path;
		// stdin
		tab[1] = cnfFile;// correctFormatForLinux(cnfFile);
		// destination, fichier de sortie
		tab[2] = param.getOut();// correctFormatForLinux(param.getOut());

		return tab;
	}

	@Override
	public boolean hasTimeout() {
		return false;
	}

	@Override
	public PreProcessorResult runPreProcessor(String[] cmd, String fileOutput, Semaphore manager) {
		PreProcessorResult res = new PreProcessorResult();

		BufferedReader input = null;
		BufferedReader inerr = null;
		try
		{// lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);

			try
			{
				process = Runtime.getRuntime().exec(cmd);
			} catch (IOException e)
			{
				throw e;
			}
			finally
			{// libere les sem
				sem.release();
				if (manager != null)
					manager.release();
			}

			String line;
			input = new BufferedReader(new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader(new InputStreamReader(process.getErrorStream()));

			while ((line = input.readLine()) != null)
			{ // verifie les stdin
				System.out.println(line);
				res.addStdin(line + "\n");
			}
			while ((line = inerr.readLine()) != null)
			{ // verifie les stderr
				System.out.println(line);
				res.addStderr(line + "\n");
			}
		} catch (IOException e)
		{
			// e.printStackTrace();
			res.setStatus(PreProcessorResultStatus.PROBLEM);
			if (process != null)
				process.destroy();
		}
		finally
		{
			try
			{
				if (input != null)
					input.close();
				if (inerr != null)
					inerr.close();
				if (process != null)
					res.setExitVal(process.waitFor());
			} catch (Exception e)
			{
				e.printStackTrace();
				res.setStatus(PreProcessorResultStatus.PROBLEM);
			}
			finally
			{
				try
				{
					sem.acquire();
				} catch (InterruptedException e)
				{
					// TODO Auto-generated catch block
					e.printStackTrace();
					return null;
				}

				setRunning(false);
			}
		}
		// terminer
		res.setEnd(System.currentTimeMillis());

		// System.out.println("val de retour"+res.getExitVal());

		// s'occupe du status
		if (hasBeenStop())
			res.setStatus(PreProcessorResultStatus.STOP);
		else
			if (hasBeenTimeout())
				res.setStatus(PreProcessorResultStatus.TIMEOUT_REACHED);
			else
				if (res.getStatus() != PreProcessorResultStatus.PROBLEM)
					if (res.getExitVal() == RETURN_UNSATISFIABLE)
						res.setStatus(PreProcessorResultStatus.UNSATISFIABLE);
					else
						if (res.getExitVal() == DEFAULT_RETURN_VALUE)
							res.setStatus(PreProcessorResultStatus.OK);
						else
							res.setStatus(PreProcessorResultStatus.PROBLEM);

		// dernier details
		res.setDescription(DESCRIPTION);
		res.setExportPath(fileOutput);
		try
		{
			if (res.getStatus() == PreProcessorResultStatus.OK)
			{
				res.setCnf(new FileCNF(fileOutput));
				// getNbLiteral(res);
				// res.setStat(new Stat(res.getCnf()));
			}
		} catch (Exception e)
		{
			// e.printStackTrace();
			res.setStatus(PreProcessorResultStatus.PROBLEM);
		}

		// libere le sem
		sem.release();

		return res;
	}

	/**
	 * Set in the {@link Stat} the number of literal using the standard output of satellite
	 * 
	 * @param res
	 *            the result of the satellite execution
	 */
	private void getNbLiteral(PreProcessorResult res) {
		String out = res.getStdin();
		Stat stat = res.getCnf().getStat();

		int begin = out.indexOf(LITERALS);
		if (begin == -1)
			return;

		begin += LITERALS.length();

		Scanner scan = new Scanner(out.substring(begin));

		// System.out.println("stdin : "+out+"\n sub : "+out.substring(begin));

		stat.setNumLiteral(scan.nextInt());
	}

}
